Guarded impredicative polymorphism